0 Prolog
↳1 PrologToDTProblemTransformerProof (⇒, 187 ms)
↳2 TRIPLES
↳3 TriplesToPiDPProof (⇒, 177 ms)
↳4 PiDP
↳5 DependencyGraphProof (⇔, 0 ms)
↳6 AND
↳7 PiDP
↳8 UsableRulesProof (⇔, 0 ms)
↳9 PiDP
↳10 PiDPToQDPProof (⇒, 33 ms)
↳11 QDP
↳12 UsableRulesReductionPairsProof (⇔, 84 ms)
↳13 QDP
↳14 QDPSizeChangeProof (⇔, 0 ms)
↳15 YES
↳16 PiDP
↳17 PiDPToQDPProof (⇒, 0 ms)
↳18 QDP
↳19 Rewriting (⇔, 0 ms)
↳20 QDP
↳21 UsableRulesProof (⇔, 0 ms)
↳22 QDP
↳23 QReductionProof (⇔, 0 ms)
↳24 QDP
↳25 QDPOrderProof (⇔, 199 ms)
↳26 QDP
↳27 DependencyGraphProof (⇔, 0 ms)
↳28 QDP
↳29 UsableRulesProof (⇔, 0 ms)
↳30 QDP
↳31 QReductionProof (⇔, 0 ms)
↳32 QDP
↳33 QDPOrderProof (⇔, 89 ms)
↳34 QDP
↳35 DependencyGraphProof (⇔, 0 ms)
↳36 TRUE
COUNTA_IN_GA(cons(atom(X1), cons(atom(X2), X3)), s(s(X4))) → U6_GA(X1, X2, X3, X4, countA_in_ga(X3, X4))
COUNTA_IN_GA(cons(atom(X1), cons(atom(X2), X3)), s(s(X4))) → COUNTA_IN_GA(X3, X4)
COUNTA_IN_GA(cons(atom(X1), cons(cons(X2, X3), X4)), s(X5)) → U7_GA(X1, X2, X3, X4, X5, flattenC_in_ggga(X2, X3, X4, X6))
COUNTA_IN_GA(cons(atom(X1), cons(cons(X2, X3), X4)), s(X5)) → FLATTENC_IN_GGGA(X2, X3, X4, X6)
FLATTENC_IN_GGGA(atom(X1), atom(X2), X3, .(X1, .(X2, X4))) → U3_GGGA(X1, X2, X3, X4, flattenD_in_ga(X3, X4))
FLATTENC_IN_GGGA(atom(X1), atom(X2), X3, .(X1, .(X2, X4))) → FLATTEND_IN_GA(X3, X4)
FLATTEND_IN_GA(cons(atom(X1), X2), .(X1, X3)) → U1_GA(X1, X2, X3, flattenD_in_ga(X2, X3))
FLATTEND_IN_GA(cons(atom(X1), X2), .(X1, X3)) → FLATTEND_IN_GA(X2, X3)
FLATTEND_IN_GA(cons(cons(X1, X2), X3), X4) → U2_GA(X1, X2, X3, X4, flattenC_in_ggga(X1, X2, X3, X4))
FLATTEND_IN_GA(cons(cons(X1, X2), X3), X4) → FLATTENC_IN_GGGA(X1, X2, X3, X4)
FLATTENC_IN_GGGA(atom(X1), cons(X2, X3), X4, .(X1, X5)) → U4_GGGA(X1, X2, X3, X4, X5, flattenC_in_ggga(X2, X3, X4, X5))
FLATTENC_IN_GGGA(atom(X1), cons(X2, X3), X4, .(X1, X5)) → FLATTENC_IN_GGGA(X2, X3, X4, X5)
FLATTENC_IN_GGGA(cons(X1, X2), X3, X4, X5) → U5_GGGA(X1, X2, X3, X4, X5, flattenC_in_ggga(X1, X2, cons(X3, X4), X5))
FLATTENC_IN_GGGA(cons(X1, X2), X3, X4, X5) → FLATTENC_IN_GGGA(X1, X2, cons(X3, X4), X5)
COUNTA_IN_GA(cons(atom(X1), cons(cons(X2, X3), X4)), s(X5)) → U8_GA(X1, X2, X3, X4, X5, flattencB_in_ggga(X2, X3, X4, X6))
U8_GA(X1, X2, X3, X4, X5, flattencB_out_ggga(X2, X3, X4, X6)) → U9_GA(X1, X2, X3, X4, X5, countA_in_ga(X6, X5))
U8_GA(X1, X2, X3, X4, X5, flattencB_out_ggga(X2, X3, X4, X6)) → COUNTA_IN_GA(X6, X5)
COUNTA_IN_GA(cons(cons(X1, X2), X3), X4) → U10_GA(X1, X2, X3, X4, flattenC_in_ggga(X1, X2, X3, X5))
COUNTA_IN_GA(cons(cons(X1, X2), X3), X4) → FLATTENC_IN_GGGA(X1, X2, X3, X5)
COUNTA_IN_GA(cons(cons(X1, X2), X3), X4) → U11_GA(X1, X2, X3, X4, flattencC_in_ggga(X1, X2, X3, X5))
U11_GA(X1, X2, X3, X4, flattencC_out_ggga(X1, X2, X3, X5)) → U12_GA(X1, X2, X3, X4, countA_in_ga(X5, X4))
U11_GA(X1, X2, X3, X4, flattencC_out_ggga(X1, X2, X3, X5)) → COUNTA_IN_GA(X5, X4)
flattencB_in_ggga(X1, X2, X3, X4) → U24_ggga(X1, X2, X3, X4, flattencC_in_ggga(X1, X2, X3, X4))
flattencC_in_ggga(atom(X1), atom(X2), X3, .(X1, .(X2, X4))) → U21_ggga(X1, X2, X3, X4, flattencD_in_ga(X3, X4))
flattencD_in_ga(atom(X1), .(X1, [])) → flattencD_out_ga(atom(X1), .(X1, []))
flattencD_in_ga(cons(atom(X1), X2), .(X1, X3)) → U19_ga(X1, X2, X3, flattencD_in_ga(X2, X3))
flattencD_in_ga(cons(cons(X1, X2), X3), X4) → U20_ga(X1, X2, X3, X4, flattencC_in_ggga(X1, X2, X3, X4))
flattencC_in_ggga(atom(X1), cons(X2, X3), X4, .(X1, X5)) → U22_ggga(X1, X2, X3, X4, X5, flattencC_in_ggga(X2, X3, X4, X5))
flattencC_in_ggga(cons(X1, X2), X3, X4, X5) → U23_ggga(X1, X2, X3, X4, X5, flattencC_in_ggga(X1, X2, cons(X3, X4), X5))
U23_ggga(X1, X2, X3, X4, X5, flattencC_out_ggga(X1, X2, cons(X3, X4), X5)) → flattencC_out_ggga(cons(X1, X2), X3, X4, X5)
U22_ggga(X1, X2, X3, X4, X5, flattencC_out_ggga(X2, X3, X4, X5)) → flattencC_out_ggga(atom(X1), cons(X2, X3), X4, .(X1, X5))
U20_ga(X1, X2, X3, X4, flattencC_out_ggga(X1, X2, X3, X4)) → flattencD_out_ga(cons(cons(X1, X2), X3), X4)
U19_ga(X1, X2, X3, flattencD_out_ga(X2, X3)) → flattencD_out_ga(cons(atom(X1), X2), .(X1, X3))
U21_ggga(X1, X2, X3, X4, flattencD_out_ga(X3, X4)) → flattencC_out_ggga(atom(X1), atom(X2), X3, .(X1, .(X2, X4)))
U24_ggga(X1, X2, X3, X4, flattencC_out_ggga(X1, X2, X3, X4)) → flattencB_out_ggga(X1, X2, X3, X4)
Infinitary Constructor Rewriting Termination of PiDP implies Termination of TRIPLES
COUNTA_IN_GA(cons(atom(X1), cons(atom(X2), X3)), s(s(X4))) → U6_GA(X1, X2, X3, X4, countA_in_ga(X3, X4))
COUNTA_IN_GA(cons(atom(X1), cons(atom(X2), X3)), s(s(X4))) → COUNTA_IN_GA(X3, X4)
COUNTA_IN_GA(cons(atom(X1), cons(cons(X2, X3), X4)), s(X5)) → U7_GA(X1, X2, X3, X4, X5, flattenC_in_ggga(X2, X3, X4, X6))
COUNTA_IN_GA(cons(atom(X1), cons(cons(X2, X3), X4)), s(X5)) → FLATTENC_IN_GGGA(X2, X3, X4, X6)
FLATTENC_IN_GGGA(atom(X1), atom(X2), X3, .(X1, .(X2, X4))) → U3_GGGA(X1, X2, X3, X4, flattenD_in_ga(X3, X4))
FLATTENC_IN_GGGA(atom(X1), atom(X2), X3, .(X1, .(X2, X4))) → FLATTEND_IN_GA(X3, X4)
FLATTEND_IN_GA(cons(atom(X1), X2), .(X1, X3)) → U1_GA(X1, X2, X3, flattenD_in_ga(X2, X3))
FLATTEND_IN_GA(cons(atom(X1), X2), .(X1, X3)) → FLATTEND_IN_GA(X2, X3)
FLATTEND_IN_GA(cons(cons(X1, X2), X3), X4) → U2_GA(X1, X2, X3, X4, flattenC_in_ggga(X1, X2, X3, X4))
FLATTEND_IN_GA(cons(cons(X1, X2), X3), X4) → FLATTENC_IN_GGGA(X1, X2, X3, X4)
FLATTENC_IN_GGGA(atom(X1), cons(X2, X3), X4, .(X1, X5)) → U4_GGGA(X1, X2, X3, X4, X5, flattenC_in_ggga(X2, X3, X4, X5))
FLATTENC_IN_GGGA(atom(X1), cons(X2, X3), X4, .(X1, X5)) → FLATTENC_IN_GGGA(X2, X3, X4, X5)
FLATTENC_IN_GGGA(cons(X1, X2), X3, X4, X5) → U5_GGGA(X1, X2, X3, X4, X5, flattenC_in_ggga(X1, X2, cons(X3, X4), X5))
FLATTENC_IN_GGGA(cons(X1, X2), X3, X4, X5) → FLATTENC_IN_GGGA(X1, X2, cons(X3, X4), X5)
COUNTA_IN_GA(cons(atom(X1), cons(cons(X2, X3), X4)), s(X5)) → U8_GA(X1, X2, X3, X4, X5, flattencB_in_ggga(X2, X3, X4, X6))
U8_GA(X1, X2, X3, X4, X5, flattencB_out_ggga(X2, X3, X4, X6)) → U9_GA(X1, X2, X3, X4, X5, countA_in_ga(X6, X5))
U8_GA(X1, X2, X3, X4, X5, flattencB_out_ggga(X2, X3, X4, X6)) → COUNTA_IN_GA(X6, X5)
COUNTA_IN_GA(cons(cons(X1, X2), X3), X4) → U10_GA(X1, X2, X3, X4, flattenC_in_ggga(X1, X2, X3, X5))
COUNTA_IN_GA(cons(cons(X1, X2), X3), X4) → FLATTENC_IN_GGGA(X1, X2, X3, X5)
COUNTA_IN_GA(cons(cons(X1, X2), X3), X4) → U11_GA(X1, X2, X3, X4, flattencC_in_ggga(X1, X2, X3, X5))
U11_GA(X1, X2, X3, X4, flattencC_out_ggga(X1, X2, X3, X5)) → U12_GA(X1, X2, X3, X4, countA_in_ga(X5, X4))
U11_GA(X1, X2, X3, X4, flattencC_out_ggga(X1, X2, X3, X5)) → COUNTA_IN_GA(X5, X4)
flattencB_in_ggga(X1, X2, X3, X4) → U24_ggga(X1, X2, X3, X4, flattencC_in_ggga(X1, X2, X3, X4))
flattencC_in_ggga(atom(X1), atom(X2), X3, .(X1, .(X2, X4))) → U21_ggga(X1, X2, X3, X4, flattencD_in_ga(X3, X4))
flattencD_in_ga(atom(X1), .(X1, [])) → flattencD_out_ga(atom(X1), .(X1, []))
flattencD_in_ga(cons(atom(X1), X2), .(X1, X3)) → U19_ga(X1, X2, X3, flattencD_in_ga(X2, X3))
flattencD_in_ga(cons(cons(X1, X2), X3), X4) → U20_ga(X1, X2, X3, X4, flattencC_in_ggga(X1, X2, X3, X4))
flattencC_in_ggga(atom(X1), cons(X2, X3), X4, .(X1, X5)) → U22_ggga(X1, X2, X3, X4, X5, flattencC_in_ggga(X2, X3, X4, X5))
flattencC_in_ggga(cons(X1, X2), X3, X4, X5) → U23_ggga(X1, X2, X3, X4, X5, flattencC_in_ggga(X1, X2, cons(X3, X4), X5))
U23_ggga(X1, X2, X3, X4, X5, flattencC_out_ggga(X1, X2, cons(X3, X4), X5)) → flattencC_out_ggga(cons(X1, X2), X3, X4, X5)
U22_ggga(X1, X2, X3, X4, X5, flattencC_out_ggga(X2, X3, X4, X5)) → flattencC_out_ggga(atom(X1), cons(X2, X3), X4, .(X1, X5))
U20_ga(X1, X2, X3, X4, flattencC_out_ggga(X1, X2, X3, X4)) → flattencD_out_ga(cons(cons(X1, X2), X3), X4)
U19_ga(X1, X2, X3, flattencD_out_ga(X2, X3)) → flattencD_out_ga(cons(atom(X1), X2), .(X1, X3))
U21_ggga(X1, X2, X3, X4, flattencD_out_ga(X3, X4)) → flattencC_out_ggga(atom(X1), atom(X2), X3, .(X1, .(X2, X4)))
U24_ggga(X1, X2, X3, X4, flattencC_out_ggga(X1, X2, X3, X4)) → flattencB_out_ggga(X1, X2, X3, X4)
FLATTENC_IN_GGGA(atom(X1), atom(X2), X3, .(X1, .(X2, X4))) → FLATTEND_IN_GA(X3, X4)
FLATTEND_IN_GA(cons(atom(X1), X2), .(X1, X3)) → FLATTEND_IN_GA(X2, X3)
FLATTEND_IN_GA(cons(cons(X1, X2), X3), X4) → FLATTENC_IN_GGGA(X1, X2, X3, X4)
FLATTENC_IN_GGGA(atom(X1), cons(X2, X3), X4, .(X1, X5)) → FLATTENC_IN_GGGA(X2, X3, X4, X5)
FLATTENC_IN_GGGA(cons(X1, X2), X3, X4, X5) → FLATTENC_IN_GGGA(X1, X2, cons(X3, X4), X5)
flattencB_in_ggga(X1, X2, X3, X4) → U24_ggga(X1, X2, X3, X4, flattencC_in_ggga(X1, X2, X3, X4))
flattencC_in_ggga(atom(X1), atom(X2), X3, .(X1, .(X2, X4))) → U21_ggga(X1, X2, X3, X4, flattencD_in_ga(X3, X4))
flattencD_in_ga(atom(X1), .(X1, [])) → flattencD_out_ga(atom(X1), .(X1, []))
flattencD_in_ga(cons(atom(X1), X2), .(X1, X3)) → U19_ga(X1, X2, X3, flattencD_in_ga(X2, X3))
flattencD_in_ga(cons(cons(X1, X2), X3), X4) → U20_ga(X1, X2, X3, X4, flattencC_in_ggga(X1, X2, X3, X4))
flattencC_in_ggga(atom(X1), cons(X2, X3), X4, .(X1, X5)) → U22_ggga(X1, X2, X3, X4, X5, flattencC_in_ggga(X2, X3, X4, X5))
flattencC_in_ggga(cons(X1, X2), X3, X4, X5) → U23_ggga(X1, X2, X3, X4, X5, flattencC_in_ggga(X1, X2, cons(X3, X4), X5))
U23_ggga(X1, X2, X3, X4, X5, flattencC_out_ggga(X1, X2, cons(X3, X4), X5)) → flattencC_out_ggga(cons(X1, X2), X3, X4, X5)
U22_ggga(X1, X2, X3, X4, X5, flattencC_out_ggga(X2, X3, X4, X5)) → flattencC_out_ggga(atom(X1), cons(X2, X3), X4, .(X1, X5))
U20_ga(X1, X2, X3, X4, flattencC_out_ggga(X1, X2, X3, X4)) → flattencD_out_ga(cons(cons(X1, X2), X3), X4)
U19_ga(X1, X2, X3, flattencD_out_ga(X2, X3)) → flattencD_out_ga(cons(atom(X1), X2), .(X1, X3))
U21_ggga(X1, X2, X3, X4, flattencD_out_ga(X3, X4)) → flattencC_out_ggga(atom(X1), atom(X2), X3, .(X1, .(X2, X4)))
U24_ggga(X1, X2, X3, X4, flattencC_out_ggga(X1, X2, X3, X4)) → flattencB_out_ggga(X1, X2, X3, X4)
FLATTENC_IN_GGGA(atom(X1), atom(X2), X3, .(X1, .(X2, X4))) → FLATTEND_IN_GA(X3, X4)
FLATTEND_IN_GA(cons(atom(X1), X2), .(X1, X3)) → FLATTEND_IN_GA(X2, X3)
FLATTEND_IN_GA(cons(cons(X1, X2), X3), X4) → FLATTENC_IN_GGGA(X1, X2, X3, X4)
FLATTENC_IN_GGGA(atom(X1), cons(X2, X3), X4, .(X1, X5)) → FLATTENC_IN_GGGA(X2, X3, X4, X5)
FLATTENC_IN_GGGA(cons(X1, X2), X3, X4, X5) → FLATTENC_IN_GGGA(X1, X2, cons(X3, X4), X5)
FLATTENC_IN_GGGA(atom(X1), atom(X2), X3) → FLATTEND_IN_GA(X3)
FLATTEND_IN_GA(cons(atom(X1), X2)) → FLATTEND_IN_GA(X2)
FLATTEND_IN_GA(cons(cons(X1, X2), X3)) → FLATTENC_IN_GGGA(X1, X2, X3)
FLATTENC_IN_GGGA(atom(X1), cons(X2, X3), X4) → FLATTENC_IN_GGGA(X2, X3, X4)
FLATTENC_IN_GGGA(cons(X1, X2), X3, X4) → FLATTENC_IN_GGGA(X1, X2, cons(X3, X4))
No rules are removed from R.
FLATTENC_IN_GGGA(atom(X1), atom(X2), X3) → FLATTEND_IN_GA(X3)
FLATTEND_IN_GA(cons(atom(X1), X2)) → FLATTEND_IN_GA(X2)
FLATTEND_IN_GA(cons(cons(X1, X2), X3)) → FLATTENC_IN_GGGA(X1, X2, X3)
FLATTENC_IN_GGGA(atom(X1), cons(X2, X3), X4) → FLATTENC_IN_GGGA(X2, X3, X4)
POL(FLATTENC_IN_GGGA(x1, x2, x3)) = 2·x1 + 2·x2 + 2·x3
POL(FLATTEND_IN_GA(x1)) = 1 + 2·x1
POL(atom(x1)) = 1 + x1
POL(cons(x1, x2)) = x1 + x2
FLATTENC_IN_GGGA(cons(X1, X2), X3, X4) → FLATTENC_IN_GGGA(X1, X2, cons(X3, X4))
From the DPs we obtained the following set of size-change graphs:
COUNTA_IN_GA(cons(atom(X1), cons(cons(X2, X3), X4)), s(X5)) → U8_GA(X1, X2, X3, X4, X5, flattencB_in_ggga(X2, X3, X4, X6))
U8_GA(X1, X2, X3, X4, X5, flattencB_out_ggga(X2, X3, X4, X6)) → COUNTA_IN_GA(X6, X5)
COUNTA_IN_GA(cons(atom(X1), cons(atom(X2), X3)), s(s(X4))) → COUNTA_IN_GA(X3, X4)
COUNTA_IN_GA(cons(cons(X1, X2), X3), X4) → U11_GA(X1, X2, X3, X4, flattencC_in_ggga(X1, X2, X3, X5))
U11_GA(X1, X2, X3, X4, flattencC_out_ggga(X1, X2, X3, X5)) → COUNTA_IN_GA(X5, X4)
flattencB_in_ggga(X1, X2, X3, X4) → U24_ggga(X1, X2, X3, X4, flattencC_in_ggga(X1, X2, X3, X4))
flattencC_in_ggga(atom(X1), atom(X2), X3, .(X1, .(X2, X4))) → U21_ggga(X1, X2, X3, X4, flattencD_in_ga(X3, X4))
flattencD_in_ga(atom(X1), .(X1, [])) → flattencD_out_ga(atom(X1), .(X1, []))
flattencD_in_ga(cons(atom(X1), X2), .(X1, X3)) → U19_ga(X1, X2, X3, flattencD_in_ga(X2, X3))
flattencD_in_ga(cons(cons(X1, X2), X3), X4) → U20_ga(X1, X2, X3, X4, flattencC_in_ggga(X1, X2, X3, X4))
flattencC_in_ggga(atom(X1), cons(X2, X3), X4, .(X1, X5)) → U22_ggga(X1, X2, X3, X4, X5, flattencC_in_ggga(X2, X3, X4, X5))
flattencC_in_ggga(cons(X1, X2), X3, X4, X5) → U23_ggga(X1, X2, X3, X4, X5, flattencC_in_ggga(X1, X2, cons(X3, X4), X5))
U23_ggga(X1, X2, X3, X4, X5, flattencC_out_ggga(X1, X2, cons(X3, X4), X5)) → flattencC_out_ggga(cons(X1, X2), X3, X4, X5)
U22_ggga(X1, X2, X3, X4, X5, flattencC_out_ggga(X2, X3, X4, X5)) → flattencC_out_ggga(atom(X1), cons(X2, X3), X4, .(X1, X5))
U20_ga(X1, X2, X3, X4, flattencC_out_ggga(X1, X2, X3, X4)) → flattencD_out_ga(cons(cons(X1, X2), X3), X4)
U19_ga(X1, X2, X3, flattencD_out_ga(X2, X3)) → flattencD_out_ga(cons(atom(X1), X2), .(X1, X3))
U21_ggga(X1, X2, X3, X4, flattencD_out_ga(X3, X4)) → flattencC_out_ggga(atom(X1), atom(X2), X3, .(X1, .(X2, X4)))
U24_ggga(X1, X2, X3, X4, flattencC_out_ggga(X1, X2, X3, X4)) → flattencB_out_ggga(X1, X2, X3, X4)
COUNTA_IN_GA(cons(atom(X1), cons(cons(X2, X3), X4))) → U8_GA(X1, X2, X3, X4, flattencB_in_ggga(X2, X3, X4))
U8_GA(X1, X2, X3, X4, flattencB_out_ggga(X2, X3, X4, X6)) → COUNTA_IN_GA(X6)
COUNTA_IN_GA(cons(atom(X1), cons(atom(X2), X3))) → COUNTA_IN_GA(X3)
COUNTA_IN_GA(cons(cons(X1, X2), X3)) → U11_GA(X1, X2, X3, flattencC_in_ggga(X1, X2, X3))
U11_GA(X1, X2, X3, flattencC_out_ggga(X1, X2, X3, X5)) → COUNTA_IN_GA(X5)
flattencB_in_ggga(X1, X2, X3) → U24_ggga(X1, X2, X3, flattencC_in_ggga(X1, X2, X3))
flattencC_in_ggga(atom(X1), atom(X2), X3) → U21_ggga(X1, X2, X3, flattencD_in_ga(X3))
flattencD_in_ga(atom(X1)) → flattencD_out_ga(atom(X1), .(X1, []))
flattencD_in_ga(cons(atom(X1), X2)) → U19_ga(X1, X2, flattencD_in_ga(X2))
flattencD_in_ga(cons(cons(X1, X2), X3)) → U20_ga(X1, X2, X3, flattencC_in_ggga(X1, X2, X3))
flattencC_in_ggga(atom(X1), cons(X2, X3), X4) → U22_ggga(X1, X2, X3, X4, flattencC_in_ggga(X2, X3, X4))
flattencC_in_ggga(cons(X1, X2), X3, X4) → U23_ggga(X1, X2, X3, X4, flattencC_in_ggga(X1, X2, cons(X3, X4)))
U23_ggga(X1, X2, X3, X4, flattencC_out_ggga(X1, X2, cons(X3, X4), X5)) → flattencC_out_ggga(cons(X1, X2), X3, X4, X5)
U22_ggga(X1, X2, X3, X4, flattencC_out_ggga(X2, X3, X4, X5)) → flattencC_out_ggga(atom(X1), cons(X2, X3), X4, .(X1, X5))
U20_ga(X1, X2, X3, flattencC_out_ggga(X1, X2, X3, X4)) → flattencD_out_ga(cons(cons(X1, X2), X3), X4)
U19_ga(X1, X2, flattencD_out_ga(X2, X3)) → flattencD_out_ga(cons(atom(X1), X2), .(X1, X3))
U21_ggga(X1, X2, X3, flattencD_out_ga(X3, X4)) → flattencC_out_ggga(atom(X1), atom(X2), X3, .(X1, .(X2, X4)))
U24_ggga(X1, X2, X3, flattencC_out_ggga(X1, X2, X3, X4)) → flattencB_out_ggga(X1, X2, X3, X4)
flattencB_in_ggga(x0, x1, x2)
flattencC_in_ggga(x0, x1, x2)
flattencD_in_ga(x0)
U23_ggga(x0, x1, x2, x3, x4)
U22_ggga(x0, x1, x2, x3, x4)
U20_ga(x0, x1, x2, x3)
U19_ga(x0, x1, x2)
U21_ggga(x0, x1, x2, x3)
U24_ggga(x0, x1, x2, x3)
COUNTA_IN_GA(cons(atom(X1), cons(cons(X2, X3), X4))) → U8_GA(X1, X2, X3, X4, U24_ggga(X2, X3, X4, flattencC_in_ggga(X2, X3, X4)))
U8_GA(X1, X2, X3, X4, flattencB_out_ggga(X2, X3, X4, X6)) → COUNTA_IN_GA(X6)
COUNTA_IN_GA(cons(atom(X1), cons(atom(X2), X3))) → COUNTA_IN_GA(X3)
COUNTA_IN_GA(cons(cons(X1, X2), X3)) → U11_GA(X1, X2, X3, flattencC_in_ggga(X1, X2, X3))
U11_GA(X1, X2, X3, flattencC_out_ggga(X1, X2, X3, X5)) → COUNTA_IN_GA(X5)
COUNTA_IN_GA(cons(atom(X1), cons(cons(X2, X3), X4))) → U8_GA(X1, X2, X3, X4, U24_ggga(X2, X3, X4, flattencC_in_ggga(X2, X3, X4)))
flattencB_in_ggga(X1, X2, X3) → U24_ggga(X1, X2, X3, flattencC_in_ggga(X1, X2, X3))
flattencC_in_ggga(atom(X1), atom(X2), X3) → U21_ggga(X1, X2, X3, flattencD_in_ga(X3))
flattencD_in_ga(atom(X1)) → flattencD_out_ga(atom(X1), .(X1, []))
flattencD_in_ga(cons(atom(X1), X2)) → U19_ga(X1, X2, flattencD_in_ga(X2))
flattencD_in_ga(cons(cons(X1, X2), X3)) → U20_ga(X1, X2, X3, flattencC_in_ggga(X1, X2, X3))
flattencC_in_ggga(atom(X1), cons(X2, X3), X4) → U22_ggga(X1, X2, X3, X4, flattencC_in_ggga(X2, X3, X4))
flattencC_in_ggga(cons(X1, X2), X3, X4) → U23_ggga(X1, X2, X3, X4, flattencC_in_ggga(X1, X2, cons(X3, X4)))
U23_ggga(X1, X2, X3, X4, flattencC_out_ggga(X1, X2, cons(X3, X4), X5)) → flattencC_out_ggga(cons(X1, X2), X3, X4, X5)
U22_ggga(X1, X2, X3, X4, flattencC_out_ggga(X2, X3, X4, X5)) → flattencC_out_ggga(atom(X1), cons(X2, X3), X4, .(X1, X5))
U20_ga(X1, X2, X3, flattencC_out_ggga(X1, X2, X3, X4)) → flattencD_out_ga(cons(cons(X1, X2), X3), X4)
U19_ga(X1, X2, flattencD_out_ga(X2, X3)) → flattencD_out_ga(cons(atom(X1), X2), .(X1, X3))
U21_ggga(X1, X2, X3, flattencD_out_ga(X3, X4)) → flattencC_out_ggga(atom(X1), atom(X2), X3, .(X1, .(X2, X4)))
U24_ggga(X1, X2, X3, flattencC_out_ggga(X1, X2, X3, X4)) → flattencB_out_ggga(X1, X2, X3, X4)
flattencB_in_ggga(x0, x1, x2)
flattencC_in_ggga(x0, x1, x2)
flattencD_in_ga(x0)
U23_ggga(x0, x1, x2, x3, x4)
U22_ggga(x0, x1, x2, x3, x4)
U20_ga(x0, x1, x2, x3)
U19_ga(x0, x1, x2)
U21_ggga(x0, x1, x2, x3)
U24_ggga(x0, x1, x2, x3)
U8_GA(X1, X2, X3, X4, flattencB_out_ggga(X2, X3, X4, X6)) → COUNTA_IN_GA(X6)
COUNTA_IN_GA(cons(atom(X1), cons(atom(X2), X3))) → COUNTA_IN_GA(X3)
COUNTA_IN_GA(cons(cons(X1, X2), X3)) → U11_GA(X1, X2, X3, flattencC_in_ggga(X1, X2, X3))
U11_GA(X1, X2, X3, flattencC_out_ggga(X1, X2, X3, X5)) → COUNTA_IN_GA(X5)
COUNTA_IN_GA(cons(atom(X1), cons(cons(X2, X3), X4))) → U8_GA(X1, X2, X3, X4, U24_ggga(X2, X3, X4, flattencC_in_ggga(X2, X3, X4)))
flattencC_in_ggga(atom(X1), atom(X2), X3) → U21_ggga(X1, X2, X3, flattencD_in_ga(X3))
flattencC_in_ggga(atom(X1), cons(X2, X3), X4) → U22_ggga(X1, X2, X3, X4, flattencC_in_ggga(X2, X3, X4))
flattencC_in_ggga(cons(X1, X2), X3, X4) → U23_ggga(X1, X2, X3, X4, flattencC_in_ggga(X1, X2, cons(X3, X4)))
U24_ggga(X1, X2, X3, flattencC_out_ggga(X1, X2, X3, X4)) → flattencB_out_ggga(X1, X2, X3, X4)
U23_ggga(X1, X2, X3, X4, flattencC_out_ggga(X1, X2, cons(X3, X4), X5)) → flattencC_out_ggga(cons(X1, X2), X3, X4, X5)
U22_ggga(X1, X2, X3, X4, flattencC_out_ggga(X2, X3, X4, X5)) → flattencC_out_ggga(atom(X1), cons(X2, X3), X4, .(X1, X5))
flattencD_in_ga(atom(X1)) → flattencD_out_ga(atom(X1), .(X1, []))
flattencD_in_ga(cons(atom(X1), X2)) → U19_ga(X1, X2, flattencD_in_ga(X2))
flattencD_in_ga(cons(cons(X1, X2), X3)) → U20_ga(X1, X2, X3, flattencC_in_ggga(X1, X2, X3))
U21_ggga(X1, X2, X3, flattencD_out_ga(X3, X4)) → flattencC_out_ggga(atom(X1), atom(X2), X3, .(X1, .(X2, X4)))
U20_ga(X1, X2, X3, flattencC_out_ggga(X1, X2, X3, X4)) → flattencD_out_ga(cons(cons(X1, X2), X3), X4)
U19_ga(X1, X2, flattencD_out_ga(X2, X3)) → flattencD_out_ga(cons(atom(X1), X2), .(X1, X3))
flattencB_in_ggga(x0, x1, x2)
flattencC_in_ggga(x0, x1, x2)
flattencD_in_ga(x0)
U23_ggga(x0, x1, x2, x3, x4)
U22_ggga(x0, x1, x2, x3, x4)
U20_ga(x0, x1, x2, x3)
U19_ga(x0, x1, x2)
U21_ggga(x0, x1, x2, x3)
U24_ggga(x0, x1, x2, x3)
flattencB_in_ggga(x0, x1, x2)
U8_GA(X1, X2, X3, X4, flattencB_out_ggga(X2, X3, X4, X6)) → COUNTA_IN_GA(X6)
COUNTA_IN_GA(cons(atom(X1), cons(atom(X2), X3))) → COUNTA_IN_GA(X3)
COUNTA_IN_GA(cons(cons(X1, X2), X3)) → U11_GA(X1, X2, X3, flattencC_in_ggga(X1, X2, X3))
U11_GA(X1, X2, X3, flattencC_out_ggga(X1, X2, X3, X5)) → COUNTA_IN_GA(X5)
COUNTA_IN_GA(cons(atom(X1), cons(cons(X2, X3), X4))) → U8_GA(X1, X2, X3, X4, U24_ggga(X2, X3, X4, flattencC_in_ggga(X2, X3, X4)))
flattencC_in_ggga(atom(X1), atom(X2), X3) → U21_ggga(X1, X2, X3, flattencD_in_ga(X3))
flattencC_in_ggga(atom(X1), cons(X2, X3), X4) → U22_ggga(X1, X2, X3, X4, flattencC_in_ggga(X2, X3, X4))
flattencC_in_ggga(cons(X1, X2), X3, X4) → U23_ggga(X1, X2, X3, X4, flattencC_in_ggga(X1, X2, cons(X3, X4)))
U24_ggga(X1, X2, X3, flattencC_out_ggga(X1, X2, X3, X4)) → flattencB_out_ggga(X1, X2, X3, X4)
U23_ggga(X1, X2, X3, X4, flattencC_out_ggga(X1, X2, cons(X3, X4), X5)) → flattencC_out_ggga(cons(X1, X2), X3, X4, X5)
U22_ggga(X1, X2, X3, X4, flattencC_out_ggga(X2, X3, X4, X5)) → flattencC_out_ggga(atom(X1), cons(X2, X3), X4, .(X1, X5))
flattencD_in_ga(atom(X1)) → flattencD_out_ga(atom(X1), .(X1, []))
flattencD_in_ga(cons(atom(X1), X2)) → U19_ga(X1, X2, flattencD_in_ga(X2))
flattencD_in_ga(cons(cons(X1, X2), X3)) → U20_ga(X1, X2, X3, flattencC_in_ggga(X1, X2, X3))
U21_ggga(X1, X2, X3, flattencD_out_ga(X3, X4)) → flattencC_out_ggga(atom(X1), atom(X2), X3, .(X1, .(X2, X4)))
U20_ga(X1, X2, X3, flattencC_out_ggga(X1, X2, X3, X4)) → flattencD_out_ga(cons(cons(X1, X2), X3), X4)
U19_ga(X1, X2, flattencD_out_ga(X2, X3)) → flattencD_out_ga(cons(atom(X1), X2), .(X1, X3))
flattencC_in_ggga(x0, x1, x2)
flattencD_in_ga(x0)
U23_ggga(x0, x1, x2, x3, x4)
U22_ggga(x0, x1, x2, x3, x4)
U20_ga(x0, x1, x2, x3)
U19_ga(x0, x1, x2)
U21_ggga(x0, x1, x2, x3)
U24_ggga(x0, x1, x2, x3)
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
COUNTA_IN_GA(cons(atom(X1), cons(atom(X2), X3))) → COUNTA_IN_GA(X3)
COUNTA_IN_GA(cons(atom(X1), cons(cons(X2, X3), X4))) → U8_GA(X1, X2, X3, X4, U24_ggga(X2, X3, X4, flattencC_in_ggga(X2, X3, X4)))
POL(.(x1, x2)) = 0
POL(COUNTA_IN_GA(x1)) = 1 + x1
POL(U11_GA(x1, x2, x3, x4)) = 1 + x4
POL(U19_ga(x1, x2, x3)) = 0
POL(U20_ga(x1, x2, x3, x4)) = x4
POL(U21_ggga(x1, x2, x3, x4)) = 0
POL(U22_ggga(x1, x2, x3, x4, x5)) = 0
POL(U23_ggga(x1, x2, x3, x4, x5)) = x5
POL(U24_ggga(x1, x2, x3, x4)) = 1 + x4
POL(U8_GA(x1, x2, x3, x4, x5)) = x4 + x5
POL([]) = 0
POL(atom(x1)) = 1
POL(cons(x1, x2)) = x1 + x2
POL(flattencB_out_ggga(x1, x2, x3, x4)) = 1 + x4
POL(flattencC_in_ggga(x1, x2, x3)) = 0
POL(flattencC_out_ggga(x1, x2, x3, x4)) = x4
POL(flattencD_in_ga(x1)) = 0
POL(flattencD_out_ga(x1, x2)) = 0
flattencC_in_ggga(atom(X1), atom(X2), X3) → U21_ggga(X1, X2, X3, flattencD_in_ga(X3))
flattencC_in_ggga(atom(X1), cons(X2, X3), X4) → U22_ggga(X1, X2, X3, X4, flattencC_in_ggga(X2, X3, X4))
flattencC_in_ggga(cons(X1, X2), X3, X4) → U23_ggga(X1, X2, X3, X4, flattencC_in_ggga(X1, X2, cons(X3, X4)))
U24_ggga(X1, X2, X3, flattencC_out_ggga(X1, X2, X3, X4)) → flattencB_out_ggga(X1, X2, X3, X4)
flattencD_in_ga(cons(atom(X1), X2)) → U19_ga(X1, X2, flattencD_in_ga(X2))
U19_ga(X1, X2, flattencD_out_ga(X2, X3)) → flattencD_out_ga(cons(atom(X1), X2), .(X1, X3))
flattencD_in_ga(cons(cons(X1, X2), X3)) → U20_ga(X1, X2, X3, flattencC_in_ggga(X1, X2, X3))
U20_ga(X1, X2, X3, flattencC_out_ggga(X1, X2, X3, X4)) → flattencD_out_ga(cons(cons(X1, X2), X3), X4)
U21_ggga(X1, X2, X3, flattencD_out_ga(X3, X4)) → flattencC_out_ggga(atom(X1), atom(X2), X3, .(X1, .(X2, X4)))
U22_ggga(X1, X2, X3, X4, flattencC_out_ggga(X2, X3, X4, X5)) → flattencC_out_ggga(atom(X1), cons(X2, X3), X4, .(X1, X5))
U23_ggga(X1, X2, X3, X4, flattencC_out_ggga(X1, X2, cons(X3, X4), X5)) → flattencC_out_ggga(cons(X1, X2), X3, X4, X5)
U8_GA(X1, X2, X3, X4, flattencB_out_ggga(X2, X3, X4, X6)) → COUNTA_IN_GA(X6)
COUNTA_IN_GA(cons(cons(X1, X2), X3)) → U11_GA(X1, X2, X3, flattencC_in_ggga(X1, X2, X3))
U11_GA(X1, X2, X3, flattencC_out_ggga(X1, X2, X3, X5)) → COUNTA_IN_GA(X5)
flattencC_in_ggga(atom(X1), atom(X2), X3) → U21_ggga(X1, X2, X3, flattencD_in_ga(X3))
flattencC_in_ggga(atom(X1), cons(X2, X3), X4) → U22_ggga(X1, X2, X3, X4, flattencC_in_ggga(X2, X3, X4))
flattencC_in_ggga(cons(X1, X2), X3, X4) → U23_ggga(X1, X2, X3, X4, flattencC_in_ggga(X1, X2, cons(X3, X4)))
U24_ggga(X1, X2, X3, flattencC_out_ggga(X1, X2, X3, X4)) → flattencB_out_ggga(X1, X2, X3, X4)
U23_ggga(X1, X2, X3, X4, flattencC_out_ggga(X1, X2, cons(X3, X4), X5)) → flattencC_out_ggga(cons(X1, X2), X3, X4, X5)
U22_ggga(X1, X2, X3, X4, flattencC_out_ggga(X2, X3, X4, X5)) → flattencC_out_ggga(atom(X1), cons(X2, X3), X4, .(X1, X5))
flattencD_in_ga(atom(X1)) → flattencD_out_ga(atom(X1), .(X1, []))
flattencD_in_ga(cons(atom(X1), X2)) → U19_ga(X1, X2, flattencD_in_ga(X2))
flattencD_in_ga(cons(cons(X1, X2), X3)) → U20_ga(X1, X2, X3, flattencC_in_ggga(X1, X2, X3))
U21_ggga(X1, X2, X3, flattencD_out_ga(X3, X4)) → flattencC_out_ggga(atom(X1), atom(X2), X3, .(X1, .(X2, X4)))
U20_ga(X1, X2, X3, flattencC_out_ggga(X1, X2, X3, X4)) → flattencD_out_ga(cons(cons(X1, X2), X3), X4)
U19_ga(X1, X2, flattencD_out_ga(X2, X3)) → flattencD_out_ga(cons(atom(X1), X2), .(X1, X3))
flattencC_in_ggga(x0, x1, x2)
flattencD_in_ga(x0)
U23_ggga(x0, x1, x2, x3, x4)
U22_ggga(x0, x1, x2, x3, x4)
U20_ga(x0, x1, x2, x3)
U19_ga(x0, x1, x2)
U21_ggga(x0, x1, x2, x3)
U24_ggga(x0, x1, x2, x3)
U11_GA(X1, X2, X3, flattencC_out_ggga(X1, X2, X3, X5)) → COUNTA_IN_GA(X5)
COUNTA_IN_GA(cons(cons(X1, X2), X3)) → U11_GA(X1, X2, X3, flattencC_in_ggga(X1, X2, X3))
flattencC_in_ggga(atom(X1), atom(X2), X3) → U21_ggga(X1, X2, X3, flattencD_in_ga(X3))
flattencC_in_ggga(atom(X1), cons(X2, X3), X4) → U22_ggga(X1, X2, X3, X4, flattencC_in_ggga(X2, X3, X4))
flattencC_in_ggga(cons(X1, X2), X3, X4) → U23_ggga(X1, X2, X3, X4, flattencC_in_ggga(X1, X2, cons(X3, X4)))
U24_ggga(X1, X2, X3, flattencC_out_ggga(X1, X2, X3, X4)) → flattencB_out_ggga(X1, X2, X3, X4)
U23_ggga(X1, X2, X3, X4, flattencC_out_ggga(X1, X2, cons(X3, X4), X5)) → flattencC_out_ggga(cons(X1, X2), X3, X4, X5)
U22_ggga(X1, X2, X3, X4, flattencC_out_ggga(X2, X3, X4, X5)) → flattencC_out_ggga(atom(X1), cons(X2, X3), X4, .(X1, X5))
flattencD_in_ga(atom(X1)) → flattencD_out_ga(atom(X1), .(X1, []))
flattencD_in_ga(cons(atom(X1), X2)) → U19_ga(X1, X2, flattencD_in_ga(X2))
flattencD_in_ga(cons(cons(X1, X2), X3)) → U20_ga(X1, X2, X3, flattencC_in_ggga(X1, X2, X3))
U21_ggga(X1, X2, X3, flattencD_out_ga(X3, X4)) → flattencC_out_ggga(atom(X1), atom(X2), X3, .(X1, .(X2, X4)))
U20_ga(X1, X2, X3, flattencC_out_ggga(X1, X2, X3, X4)) → flattencD_out_ga(cons(cons(X1, X2), X3), X4)
U19_ga(X1, X2, flattencD_out_ga(X2, X3)) → flattencD_out_ga(cons(atom(X1), X2), .(X1, X3))
flattencC_in_ggga(x0, x1, x2)
flattencD_in_ga(x0)
U23_ggga(x0, x1, x2, x3, x4)
U22_ggga(x0, x1, x2, x3, x4)
U20_ga(x0, x1, x2, x3)
U19_ga(x0, x1, x2)
U21_ggga(x0, x1, x2, x3)
U24_ggga(x0, x1, x2, x3)
U11_GA(X1, X2, X3, flattencC_out_ggga(X1, X2, X3, X5)) → COUNTA_IN_GA(X5)
COUNTA_IN_GA(cons(cons(X1, X2), X3)) → U11_GA(X1, X2, X3, flattencC_in_ggga(X1, X2, X3))
flattencC_in_ggga(atom(X1), atom(X2), X3) → U21_ggga(X1, X2, X3, flattencD_in_ga(X3))
flattencC_in_ggga(atom(X1), cons(X2, X3), X4) → U22_ggga(X1, X2, X3, X4, flattencC_in_ggga(X2, X3, X4))
flattencC_in_ggga(cons(X1, X2), X3, X4) → U23_ggga(X1, X2, X3, X4, flattencC_in_ggga(X1, X2, cons(X3, X4)))
U23_ggga(X1, X2, X3, X4, flattencC_out_ggga(X1, X2, cons(X3, X4), X5)) → flattencC_out_ggga(cons(X1, X2), X3, X4, X5)
U22_ggga(X1, X2, X3, X4, flattencC_out_ggga(X2, X3, X4, X5)) → flattencC_out_ggga(atom(X1), cons(X2, X3), X4, .(X1, X5))
flattencD_in_ga(atom(X1)) → flattencD_out_ga(atom(X1), .(X1, []))
flattencD_in_ga(cons(atom(X1), X2)) → U19_ga(X1, X2, flattencD_in_ga(X2))
flattencD_in_ga(cons(cons(X1, X2), X3)) → U20_ga(X1, X2, X3, flattencC_in_ggga(X1, X2, X3))
U21_ggga(X1, X2, X3, flattencD_out_ga(X3, X4)) → flattencC_out_ggga(atom(X1), atom(X2), X3, .(X1, .(X2, X4)))
U20_ga(X1, X2, X3, flattencC_out_ggga(X1, X2, X3, X4)) → flattencD_out_ga(cons(cons(X1, X2), X3), X4)
U19_ga(X1, X2, flattencD_out_ga(X2, X3)) → flattencD_out_ga(cons(atom(X1), X2), .(X1, X3))
flattencC_in_ggga(x0, x1, x2)
flattencD_in_ga(x0)
U23_ggga(x0, x1, x2, x3, x4)
U22_ggga(x0, x1, x2, x3, x4)
U20_ga(x0, x1, x2, x3)
U19_ga(x0, x1, x2)
U21_ggga(x0, x1, x2, x3)
U24_ggga(x0, x1, x2, x3)
U24_ggga(x0, x1, x2, x3)
U11_GA(X1, X2, X3, flattencC_out_ggga(X1, X2, X3, X5)) → COUNTA_IN_GA(X5)
COUNTA_IN_GA(cons(cons(X1, X2), X3)) → U11_GA(X1, X2, X3, flattencC_in_ggga(X1, X2, X3))
flattencC_in_ggga(atom(X1), atom(X2), X3) → U21_ggga(X1, X2, X3, flattencD_in_ga(X3))
flattencC_in_ggga(atom(X1), cons(X2, X3), X4) → U22_ggga(X1, X2, X3, X4, flattencC_in_ggga(X2, X3, X4))
flattencC_in_ggga(cons(X1, X2), X3, X4) → U23_ggga(X1, X2, X3, X4, flattencC_in_ggga(X1, X2, cons(X3, X4)))
U23_ggga(X1, X2, X3, X4, flattencC_out_ggga(X1, X2, cons(X3, X4), X5)) → flattencC_out_ggga(cons(X1, X2), X3, X4, X5)
U22_ggga(X1, X2, X3, X4, flattencC_out_ggga(X2, X3, X4, X5)) → flattencC_out_ggga(atom(X1), cons(X2, X3), X4, .(X1, X5))
flattencD_in_ga(atom(X1)) → flattencD_out_ga(atom(X1), .(X1, []))
flattencD_in_ga(cons(atom(X1), X2)) → U19_ga(X1, X2, flattencD_in_ga(X2))
flattencD_in_ga(cons(cons(X1, X2), X3)) → U20_ga(X1, X2, X3, flattencC_in_ggga(X1, X2, X3))
U21_ggga(X1, X2, X3, flattencD_out_ga(X3, X4)) → flattencC_out_ggga(atom(X1), atom(X2), X3, .(X1, .(X2, X4)))
U20_ga(X1, X2, X3, flattencC_out_ggga(X1, X2, X3, X4)) → flattencD_out_ga(cons(cons(X1, X2), X3), X4)
U19_ga(X1, X2, flattencD_out_ga(X2, X3)) → flattencD_out_ga(cons(atom(X1), X2), .(X1, X3))
flattencC_in_ggga(x0, x1, x2)
flattencD_in_ga(x0)
U23_ggga(x0, x1, x2, x3, x4)
U22_ggga(x0, x1, x2, x3, x4)
U20_ga(x0, x1, x2, x3)
U19_ga(x0, x1, x2)
U21_ggga(x0, x1, x2, x3)
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
COUNTA_IN_GA(cons(cons(X1, X2), X3)) → U11_GA(X1, X2, X3, flattencC_in_ggga(X1, X2, X3))
POL(.(x1, x2)) = 0
POL(COUNTA_IN_GA(x1)) = x1
POL(U11_GA(x1, x2, x3, x4)) = x4
POL(U19_ga(x1, x2, x3)) = 1
POL(U20_ga(x1, x2, x3, x4)) = 0
POL(U21_ggga(x1, x2, x3, x4)) = 0
POL(U22_ggga(x1, x2, x3, x4, x5)) = x5
POL(U23_ggga(x1, x2, x3, x4, x5)) = x5
POL([]) = 0
POL(atom(x1)) = 0
POL(cons(x1, x2)) = 1 + x1 + x2
POL(flattencC_in_ggga(x1, x2, x3)) = 0
POL(flattencC_out_ggga(x1, x2, x3, x4)) = x4
POL(flattencD_in_ga(x1)) = x1
POL(flattencD_out_ga(x1, x2)) = 0
flattencC_in_ggga(atom(X1), atom(X2), X3) → U21_ggga(X1, X2, X3, flattencD_in_ga(X3))
flattencC_in_ggga(atom(X1), cons(X2, X3), X4) → U22_ggga(X1, X2, X3, X4, flattencC_in_ggga(X2, X3, X4))
flattencC_in_ggga(cons(X1, X2), X3, X4) → U23_ggga(X1, X2, X3, X4, flattencC_in_ggga(X1, X2, cons(X3, X4)))
flattencD_in_ga(cons(atom(X1), X2)) → U19_ga(X1, X2, flattencD_in_ga(X2))
U19_ga(X1, X2, flattencD_out_ga(X2, X3)) → flattencD_out_ga(cons(atom(X1), X2), .(X1, X3))
flattencD_in_ga(cons(cons(X1, X2), X3)) → U20_ga(X1, X2, X3, flattencC_in_ggga(X1, X2, X3))
U20_ga(X1, X2, X3, flattencC_out_ggga(X1, X2, X3, X4)) → flattencD_out_ga(cons(cons(X1, X2), X3), X4)
U21_ggga(X1, X2, X3, flattencD_out_ga(X3, X4)) → flattencC_out_ggga(atom(X1), atom(X2), X3, .(X1, .(X2, X4)))
U22_ggga(X1, X2, X3, X4, flattencC_out_ggga(X2, X3, X4, X5)) → flattencC_out_ggga(atom(X1), cons(X2, X3), X4, .(X1, X5))
U23_ggga(X1, X2, X3, X4, flattencC_out_ggga(X1, X2, cons(X3, X4), X5)) → flattencC_out_ggga(cons(X1, X2), X3, X4, X5)
U11_GA(X1, X2, X3, flattencC_out_ggga(X1, X2, X3, X5)) → COUNTA_IN_GA(X5)
flattencC_in_ggga(atom(X1), atom(X2), X3) → U21_ggga(X1, X2, X3, flattencD_in_ga(X3))
flattencC_in_ggga(atom(X1), cons(X2, X3), X4) → U22_ggga(X1, X2, X3, X4, flattencC_in_ggga(X2, X3, X4))
flattencC_in_ggga(cons(X1, X2), X3, X4) → U23_ggga(X1, X2, X3, X4, flattencC_in_ggga(X1, X2, cons(X3, X4)))
U23_ggga(X1, X2, X3, X4, flattencC_out_ggga(X1, X2, cons(X3, X4), X5)) → flattencC_out_ggga(cons(X1, X2), X3, X4, X5)
U22_ggga(X1, X2, X3, X4, flattencC_out_ggga(X2, X3, X4, X5)) → flattencC_out_ggga(atom(X1), cons(X2, X3), X4, .(X1, X5))
flattencD_in_ga(atom(X1)) → flattencD_out_ga(atom(X1), .(X1, []))
flattencD_in_ga(cons(atom(X1), X2)) → U19_ga(X1, X2, flattencD_in_ga(X2))
flattencD_in_ga(cons(cons(X1, X2), X3)) → U20_ga(X1, X2, X3, flattencC_in_ggga(X1, X2, X3))
U21_ggga(X1, X2, X3, flattencD_out_ga(X3, X4)) → flattencC_out_ggga(atom(X1), atom(X2), X3, .(X1, .(X2, X4)))
U20_ga(X1, X2, X3, flattencC_out_ggga(X1, X2, X3, X4)) → flattencD_out_ga(cons(cons(X1, X2), X3), X4)
U19_ga(X1, X2, flattencD_out_ga(X2, X3)) → flattencD_out_ga(cons(atom(X1), X2), .(X1, X3))
flattencC_in_ggga(x0, x1, x2)
flattencD_in_ga(x0)
U23_ggga(x0, x1, x2, x3, x4)
U22_ggga(x0, x1, x2, x3, x4)
U20_ga(x0, x1, x2, x3)
U19_ga(x0, x1, x2)
U21_ggga(x0, x1, x2, x3)